COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	More bugs:  Why does the last step lose?
C00004 ENDMK
C⊗;
More bugs:  Why does the last step lose?

.RU PROOF

Saving input on: BACKUP.TMP

*****SHOW PROOF;

*****∧I INDUCTION2;

1 ∀X.((NULL X∨(CDR X*NILL)=CDR X)⊃(X*NILL)=X)⊃∀X.(X*NILL)=X  

*****∀E APPEND X,NILL;

2 (X*NILL)=IF NULL X THEN NILL ELSE CONS(CAR X,CDR X*NILL)  

*****;

3 IF NULL X THEN NILL ELSE CONS(CAR X,CDR X*NILL)=(X*NILL)≡IF NULL X %
THEN NILL=(X*NILL) ELSE CONS(CAR X,CDR X*NILL)=(X*NILL)  

*****TAUT 3:#2≡(NULL X⊃=(NILL,X*NILL))∧(¬(NULL X)⊃=(CONS(CAR X,(CDR X)*NILL),X*NILL)
);

Not a tautology

*****↑C